FDL - Nuprl Lemma : h-order_transitivity

Nuprl Lemma : h-order_transitivity

es:ES, P:(E

), H:({e:E| P(e)}

({e:E| P(e)} List)).
h-ordered(es;e.P(e);H)

(

a, b, c:{e:E| P(e)} . (a

H(b))

(b

H(c))

(a

H(c)))

Definitions x. t(x), S T, t T, P Q, x(s), , x:A. B(x), P & Q, h-ordered(es;e.P(e);H)

Lemmas event system wf, h-ordered wf, es-E wf, l member wf, iseg member